Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parity in Counterexample-Related Z3 Options for Command-Line vs Language Server #4792

Merged
merged 15 commits into from
Jan 22, 2024

Conversation

Dargones
Copy link
Collaborator

@Dargones Dargones commented Nov 16, 2023

Description

The language server supports counterexample extraction by default but command line Dafny does not, which leads to a mismatch in Z3 options. This PR ensures parity between counterexample-related options and updates counterexample extraction command line interface so that it works out of the box without requiring additional options.

How has this been tested?

There are existing tests for counterexamples that this PR should pass.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

atomb
atomb previously approved these changes Nov 16, 2023
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks very nice. It should also help reduce the differences in verification behavior between the IDE and CLI.

@@ -84,25 +84,6 @@ internal enum Status { Success, Failure, Untested }
/// Setup DafnyOptions to prepare for counterexample extraction
/// </summary>
private static void SetupForCounterexamples(DafnyOptions options) {
// Figure out the Z3 version in use:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice that this isn't necessary anymore!

@atomb
Copy link
Member

atomb commented Nov 16, 2023

Noting as we discussed earlier: let's not merge this until after 4.4 since it changes verification behavior.

@Dargones Dargones marked this pull request as ready for review January 19, 2024 15:15
@Dargones Dargones marked this pull request as draft January 19, 2024 15:16
@Dargones Dargones marked this pull request as ready for review January 22, 2024 17:44
@Dargones
Copy link
Collaborator Author

The PR is now ready to be merged. Note that it does update the Boogie version and Z3 options used for verification.

@Dargones
Copy link
Collaborator Author

Dargones commented Jan 22, 2024

@atomb, it appears that this PR might affect the way some assertion violations are reported by Dafny. In particular, I had to update this test's expected output. Does that appear to be a desirable change in behavior? This is the only test so affected. As far as I understand, the new changes cause an additional {:captureState} assumption to be inserted in the beginning of the method -- hence the change in expected output. I am not quite sure why the difference shows up for this particular test but nowhere else.

For what it is worth, when I attempt verifying this test in the VS Code, the IDE reports an error at the same location where the command line will report it once this PR is merged. So the PR definitely improves parity between the two.

@@ -1146,6 +1147,13 @@ public enum IncludesModes {
SetZ3Option("type_check", "true");
SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering
SetZ3Option("smt.delay_units", "true");
SetZ3Option("model_evaluator.completion", "true");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do these Z3 options not significantly change verification behavior?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They are on by default in the Language Server already, so I don't think they should.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does it matter whether they're on in the language server? They may still cause different verification behavior on the CLI.

Copy link
Collaborator Author

@Dargones Dargones Jan 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These options are meant to only affect the way Z3 processes its counterexample model, so the result of verification will stay the same. I believe @atomb looked into variability data as well, so there are no unexpected performance-related problems. The fact that these options have been used by the Language Server for over two years just means that there are no bugs (that we know of) associated with these options.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good, thanks!

Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

@atomb atomb merged commit fecf783 into dafny-lang:master Jan 22, 2024
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants